Trait isotope::term::Substitute[][src]

pub trait Substitute: Cons {
    type Substituted;
    fn subst_rec(
        &self,
        ctx: &mut impl SubstCtx + ?Sized
    ) -> Result<Option<Self::Substituted>, Error>;
fn from_consed(
        this: Self::Consed,
        ctx: &mut impl ConsCtx + ?Sized
    ) -> Self::Substituted; fn shift(
        &self,
        shift: i32,
        base: u32,
        ctx: &mut impl ConsCtx + ?Sized
    ) -> Result<Option<Self::Substituted>, Error> { ... }
fn shifted(
        &self,
        shift: i32,
        base: u32,
        ctx: &mut impl ConsCtx + ?Sized
    ) -> Result<Self::Substituted, Error> { ... }
fn subst_vals<B>(
        &self,
        vals: &[B],
        base: u32,
        ctx: &mut impl TyCtxMut + ?Sized
    ) -> Result<Option<Self::Substituted>, Error>
    where
        B: Borrow<TermId>
, { ... } }
Expand description

Objects which can be substituted in a context

Associated Types

The type this substitutes to

Required methods

Substitute this value recursively

Convert this object’s consed form to it’s substituted form

Provided methods

Shift this term’s variables with index >= base in a given context

Shift this term’s variables with index >= base in a given context

Substitute this term’s variables with index >= base down a variable in a given context

Implementations on Foreign Types

Implementors